f3(true, x, y) -> f3(gt2(x, y), x, round1(s1(y)))
round1(0) -> 0
round1(s1(0)) -> s1(s1(0))
round1(s1(s1(x))) -> s1(s1(round1(x)))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
round1(s1(s1(x0)))
round1(0)
gt2(0, x0)
round1(s1(0))
gt2(s1(x0), s1(x1))
f3(true, x0, x1)
gt2(s1(x0), 0)
↳ QTRS
↳ DependencyPairsProof
f3(true, x, y) -> f3(gt2(x, y), x, round1(s1(y)))
round1(0) -> 0
round1(s1(0)) -> s1(s1(0))
round1(s1(s1(x))) -> s1(s1(round1(x)))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
round1(s1(s1(x0)))
round1(0)
gt2(0, x0)
round1(s1(0))
gt2(s1(x0), s1(x1))
f3(true, x0, x1)
gt2(s1(x0), 0)
F3(true, x, y) -> F3(gt2(x, y), x, round1(s1(y)))
F3(true, x, y) -> GT2(x, y)
F3(true, x, y) -> ROUND1(s1(y))
GT2(s1(u), s1(v)) -> GT2(u, v)
ROUND1(s1(s1(x))) -> ROUND1(x)
f3(true, x, y) -> f3(gt2(x, y), x, round1(s1(y)))
round1(0) -> 0
round1(s1(0)) -> s1(s1(0))
round1(s1(s1(x))) -> s1(s1(round1(x)))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
round1(s1(s1(x0)))
round1(0)
gt2(0, x0)
round1(s1(0))
gt2(s1(x0), s1(x1))
f3(true, x0, x1)
gt2(s1(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
F3(true, x, y) -> F3(gt2(x, y), x, round1(s1(y)))
F3(true, x, y) -> GT2(x, y)
F3(true, x, y) -> ROUND1(s1(y))
GT2(s1(u), s1(v)) -> GT2(u, v)
ROUND1(s1(s1(x))) -> ROUND1(x)
f3(true, x, y) -> f3(gt2(x, y), x, round1(s1(y)))
round1(0) -> 0
round1(s1(0)) -> s1(s1(0))
round1(s1(s1(x))) -> s1(s1(round1(x)))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
round1(s1(s1(x0)))
round1(0)
gt2(0, x0)
round1(s1(0))
gt2(s1(x0), s1(x1))
f3(true, x0, x1)
gt2(s1(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
GT2(s1(u), s1(v)) -> GT2(u, v)
f3(true, x, y) -> f3(gt2(x, y), x, round1(s1(y)))
round1(0) -> 0
round1(s1(0)) -> s1(s1(0))
round1(s1(s1(x))) -> s1(s1(round1(x)))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
round1(s1(s1(x0)))
round1(0)
gt2(0, x0)
round1(s1(0))
gt2(s1(x0), s1(x1))
f3(true, x0, x1)
gt2(s1(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
GT2(s1(u), s1(v)) -> GT2(u, v)
round1(s1(s1(x0)))
round1(0)
gt2(0, x0)
round1(s1(0))
gt2(s1(x0), s1(x1))
f3(true, x0, x1)
gt2(s1(x0), 0)
round1(s1(s1(x0)))
round1(0)
gt2(0, x0)
round1(s1(0))
gt2(s1(x0), s1(x1))
f3(true, x0, x1)
gt2(s1(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
GT2(s1(u), s1(v)) -> GT2(u, v)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
ROUND1(s1(s1(x))) -> ROUND1(x)
f3(true, x, y) -> f3(gt2(x, y), x, round1(s1(y)))
round1(0) -> 0
round1(s1(0)) -> s1(s1(0))
round1(s1(s1(x))) -> s1(s1(round1(x)))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
round1(s1(s1(x0)))
round1(0)
gt2(0, x0)
round1(s1(0))
gt2(s1(x0), s1(x1))
f3(true, x0, x1)
gt2(s1(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
ROUND1(s1(s1(x))) -> ROUND1(x)
round1(s1(s1(x0)))
round1(0)
gt2(0, x0)
round1(s1(0))
gt2(s1(x0), s1(x1))
f3(true, x0, x1)
gt2(s1(x0), 0)
round1(s1(s1(x0)))
round1(0)
gt2(0, x0)
round1(s1(0))
gt2(s1(x0), s1(x1))
f3(true, x0, x1)
gt2(s1(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
ROUND1(s1(s1(x))) -> ROUND1(x)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
F3(true, x, y) -> F3(gt2(x, y), x, round1(s1(y)))
f3(true, x, y) -> f3(gt2(x, y), x, round1(s1(y)))
round1(0) -> 0
round1(s1(0)) -> s1(s1(0))
round1(s1(s1(x))) -> s1(s1(round1(x)))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
round1(s1(s1(x0)))
round1(0)
gt2(0, x0)
round1(s1(0))
gt2(s1(x0), s1(x1))
f3(true, x0, x1)
gt2(s1(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ UsableRulesProof
F3(true, x, y) -> F3(gt2(x, y), x, round1(s1(y)))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
round1(s1(0)) -> s1(s1(0))
round1(s1(s1(x))) -> s1(s1(round1(x)))
round1(0) -> 0
round1(s1(s1(x0)))
round1(0)
gt2(0, x0)
round1(s1(0))
gt2(s1(x0), s1(x1))
f3(true, x0, x1)
gt2(s1(x0), 0)
f3(true, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ UsableRulesProof
F3(true, x, y) -> F3(gt2(x, y), x, round1(s1(y)))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
round1(s1(0)) -> s1(s1(0))
round1(s1(s1(x))) -> s1(s1(round1(x)))
round1(0) -> 0
round1(s1(s1(x0)))
round1(0)
gt2(0, x0)
round1(s1(0))
gt2(s1(x0), s1(x1))
gt2(s1(x0), 0)
F3(true, s1(x0), s1(x1)) -> F3(gt2(x0, x1), s1(x0), round1(s1(s1(x1))))
F3(true, s1(x0), 0) -> F3(true, s1(x0), round1(s1(0)))
F3(true, 0, x0) -> F3(false, 0, round1(s1(x0)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ UsableRulesProof
F3(true, s1(x0), 0) -> F3(true, s1(x0), round1(s1(0)))
F3(true, s1(x0), s1(x1)) -> F3(gt2(x0, x1), s1(x0), round1(s1(s1(x1))))
F3(true, 0, x0) -> F3(false, 0, round1(s1(x0)))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
round1(s1(0)) -> s1(s1(0))
round1(s1(s1(x))) -> s1(s1(round1(x)))
round1(0) -> 0
round1(s1(s1(x0)))
round1(0)
gt2(0, x0)
round1(s1(0))
gt2(s1(x0), s1(x1))
gt2(s1(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ UsableRulesProof
F3(true, s1(x0), 0) -> F3(true, s1(x0), round1(s1(0)))
F3(true, s1(x0), s1(x1)) -> F3(gt2(x0, x1), s1(x0), round1(s1(s1(x1))))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
round1(s1(0)) -> s1(s1(0))
round1(s1(s1(x))) -> s1(s1(round1(x)))
round1(0) -> 0
round1(s1(s1(x0)))
round1(0)
gt2(0, x0)
round1(s1(0))
gt2(s1(x0), s1(x1))
gt2(s1(x0), 0)
F3(true, s1(x0), s1(x1)) -> F3(gt2(x0, x1), s1(x0), s1(s1(round1(x1))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ UsableRulesProof
F3(true, s1(x0), 0) -> F3(true, s1(x0), round1(s1(0)))
F3(true, s1(x0), s1(x1)) -> F3(gt2(x0, x1), s1(x0), s1(s1(round1(x1))))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
round1(s1(0)) -> s1(s1(0))
round1(s1(s1(x))) -> s1(s1(round1(x)))
round1(0) -> 0
round1(s1(s1(x0)))
round1(0)
gt2(0, x0)
round1(s1(0))
gt2(s1(x0), s1(x1))
gt2(s1(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ UsableRulesProof
F3(true, s1(x0), s1(x1)) -> F3(gt2(x0, x1), s1(x0), s1(s1(round1(x1))))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
round1(s1(0)) -> s1(s1(0))
round1(s1(s1(x))) -> s1(s1(round1(x)))
round1(0) -> 0
round1(s1(s1(x0)))
round1(0)
gt2(0, x0)
round1(s1(0))
gt2(s1(x0), s1(x1))
gt2(s1(x0), 0)
F3(true, s1(z0), s1(s1(y_1))) -> F3(gt2(z0, s1(y_1)), s1(z0), s1(s1(round1(s1(y_1)))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ UsableRulesProof
F3(true, s1(z0), s1(s1(y_1))) -> F3(gt2(z0, s1(y_1)), s1(z0), s1(s1(round1(s1(y_1)))))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
round1(s1(0)) -> s1(s1(0))
round1(s1(s1(x))) -> s1(s1(round1(x)))
round1(0) -> 0
round1(s1(s1(x0)))
round1(0)
gt2(0, x0)
round1(s1(0))
gt2(s1(x0), s1(x1))
gt2(s1(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
F3(true, x, y) -> F3(gt2(x, y), x, round1(s1(y)))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
round1(s1(0)) -> s1(s1(0))
round1(s1(s1(x))) -> s1(s1(round1(x)))
round1(0) -> 0
round1(s1(s1(x0)))
round1(0)
gt2(0, x0)
round1(s1(0))
gt2(s1(x0), s1(x1))
f3(true, x0, x1)
gt2(s1(x0), 0)
f3(true, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
F3(true, x, y) -> F3(gt2(x, y), x, round1(s1(y)))
gt2(0, v) -> false
gt2(s1(u), 0) -> true
gt2(s1(u), s1(v)) -> gt2(u, v)
round1(s1(0)) -> s1(s1(0))
round1(s1(s1(x))) -> s1(s1(round1(x)))
round1(0) -> 0
round1(s1(s1(x0)))
round1(0)
gt2(0, x0)
round1(s1(0))
gt2(s1(x0), s1(x1))
gt2(s1(x0), 0)